/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30/FONT#10=ZERO30/FONT#11=BAXI30



␈↓ ↓H␈↓αExpressing theorems about recursion in set theory.

␈↓ ↓H␈↓␈↓ α_The␈α
object␈α
of␈α
these␈αnotes␈α
is␈α
to␈α
explore␈α
the␈αpossibility␈α
of␈α
doing␈α
program␈α
correctness␈αproofs␈α
in
␈↓ ↓H␈↓set␈α∀theory␈α∀beginning␈α∪with␈α∀the␈α∀basic␈α∪theorems␈α∀on␈α∀the␈α∪existence␈α∀and␈α∀properties␈α∀of␈α∪recursive
␈↓ ↓H␈↓functions.

␈↓ ↓H␈↓␈↓ α_Halmos (1960) proves the following "recursion theorem".

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓∀a g X.aεX ∧ gεX␈↓#
X␈↓# ⊃ ∃f.fεX␈↓#
q␈↓#w ∧ f(0) = a ∧ ∀n.nε␈↓	w␈↓↓ ⊃ f(n') = g(f(n))␈↓.

␈↓ ↓H␈↓␈↓ α_In a LISP-like language ␈↓↓f␈↓ would be defined recursively by

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓f(n) ← ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ g(f(n-1))␈↓.

␈↓ ↓H␈↓The following are alternative definitions of ␈↓↓f:␈↓

␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓f = {u ε ␈↓	w␈↓↓␈↓πx␈↓↓X|∀z.((<0,a> ε z ∧ ∀n x.(<n,x> ε z ⊃ <n',g(x)> ε z)) ⊃ u ε z)}␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓f = ␈↓π∩␈↓↓{z ε P(␈↓	w␈↓↓ ␈↓πx␈↓↓ X)|<0,a> ε z ∧ ∀n.(<n,x> ε z ⊃ <n',g(x)> ε z)} ␈↓.

␈↓ ↓H␈↓We must then prove

␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓∀n.∃!x.(<n,x> ε f)␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓∀n x.(<n,x> ε f ≡ (n=0 ∧ x=a ∨ n≠0 ∧ ∃x1.(<n-1,x1> ε f ∧ x = g(x1)))) ␈↓.

␈↓ ↓H␈↓␈↓ α_There␈α
is␈α
a␈αdirect␈α
generalization␈α
of␈α
(1)␈αwhich␈α
does␈α
not␈α
presuppose␈αthe␈α
existence␈α
of␈α
the␈αset␈α
␈↓↓X,␈↓
␈↓ ↓H␈↓namely

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓∀x ∃!y.P(x,y) ⊃ ∀a.∃X f.aεX ∧ fεX␈↓#
q␈↓#w ∧ f(0) = a ∧ ∀n.(nε␈↓	w␈↓↓ ⊃ P(f(n),f(n')))␈↓.

␈↓ ↓H␈↓␈↓ α_The␈αproof␈αof␈α(7)␈αuses␈αquite␈αa␈αbit␈αof␈αset␈αtheoretic␈αmachinery␈αand␈αis␈αworth␈αstudying,␈αbecause
␈↓ ↓H␈↓we will need the machinery later.

␈↓ ↓H␈↓References:

␈↓ ↓H␈↓␈↓αHalmos, Paul R.␈↓ (1960) ␈↓↓Naive Set Theory␈↓